Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar3/TRCSRSLASHEx3_3_25_Bor03

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

app₂(nil, YS) -> YS
app₂(cons₁(X), YS) -> cons₁(X)
from₁(X) -> cons₁(X)
zWadr₂(nil, YS) -> nil
zWadr₂(XS, nil) -> nil
zWadr₂(cons₁(X), cons₁(Y)) -> cons₁(app₂(Y, cons₁(X)))
prefix₁(L) -> cons₁(nil)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app₂(nil, YS) -> YS
app₂(cons₁(X), YS) -> cons₁(X)
from₁(X) -> cons₁(X)
zWadr₂(nil, YS) -> nil
zWadr₂(XS, nil) -> nil
zWadr₂(cons₁(X), cons₁(Y)) -> cons₁(app₂(Y, cons₁(X)))
prefix₁(L) -> cons₁(nil)

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

ZWADR₂(cons₁(X), cons₁(Y)) -> APP₂(Y, cons₁(X))

The TRS R consists of the following rules:

app₂(nil, YS) -> YS
app₂(cons₁(X), YS) -> cons₁(X)
from₁(X) -> cons₁(X)
zWadr₂(nil, YS) -> nil
zWadr₂(XS, nil) -> nil
zWadr₂(cons₁(X), cons₁(Y)) -> cons₁(app₂(Y, cons₁(X)))
prefix₁(L) -> cons₁(nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ZWADR₂(cons₁(X), cons₁(Y)) -> APP₂(Y, cons₁(X))

The TRS R consists of the following rules:

app₂(nil, YS) -> YS
app₂(cons₁(X), YS) -> cons₁(X)
from₁(X) -> cons₁(X)
zWadr₂(nil, YS) -> nil
zWadr₂(XS, nil) -> nil
zWadr₂(cons₁(X), cons₁(Y)) -> cons₁(app₂(Y, cons₁(X)))
prefix₁(L) -> cons₁(nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.